es:ES, a:Atom1, e:E. e sends || a   

latex

Definitions	P  Q, e sends || a, , t  T, x:A. B(x)
Lemmas	event system wf, es-val wf, es-valtype wf, free-from-atom wf1, es-sender wf, es-isrcv wf, assert wf, es-E wf